Termination Proof Script

• Consider the SCC {37,50}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 37 is weakly decreasing and rule 50 is strictly decreasing. There is one new SCC.
  • Consider the SCC {37}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 37 is strictly decreasing.


• Consider the SCC {36,49}. There are no usable rules. By taking the AF π with π(F) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 36 is weakly decreasing and rule 49 is strictly decreasing. There is one new SCC.
  • Consider the SCC {36}. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 36 is strictly decreasing.


• Consider the SCC {39,52}. There are no usable rules. By taking the AF π with π(mark) = π(P) = 1 together with the lexicographic path order with empty precedence, rule 39 is weakly decreasing and rule 52 is strictly decreasing. There is one new SCC.
  • Consider the SCC {39}. By taking the AF π with π(P) = 1 together with the lexicographic path order with empty precedence, rule 39 is strictly decreasing.


• Consider the SCC {38,51}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 38 is weakly decreasing and rule 51 is strictly decreasing. There is one new SCC.
  • Consider the SCC {38}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 38 is strictly decreasing.


• Consider the SCC {41,43,44,46,48}. There are no usable rules. By taking the AF π with π(f) = π(p) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {41,46,48} are weakly decreasing and the rules in {43,44} are strictly decreasing. There is one new SCC.
  • Consider the SCC {41,46,48}. By taking the AF π with π(f) = π(p) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {41,48} are weakly decreasing and rule 46 is strictly decreasing. There is one new SCC.
    • Consider the SCC {41,48}. By taking the AF π with π(f) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 41 is weakly decreasing and rule 48 is strictly decreasing. There is one new SCC.
      • Consider the SCC {41}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 41 is strictly decreasing.


• Consider the SCC {29,31,33,35}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = π(f) = π(p) = 1 together with the lexicographic path order with empty precedence, the rules in {29,31,35} are weakly decreasing and rule 33 is strictly decreasing. There is one new SCC.
  • Consider the SCC {29,31,35}. By taking the AF π with π(ACTIVE) = π(cons) = π(f) = 1 together with the lexicographic path order with empty precedence, the rules in {29,31} are weakly decreasing and rule 35 is strictly decreasing. There is one new SCC.
    • Consider the SCC {29,31}. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 31 is weakly decreasing and rule 29 is strictly decreasing. There is one new SCC.
      • Consider the SCC {31}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 31 is strictly decreasing.


• Consider the SCC {53,55}. The usable rules are {1-20}. The constraints could not be solved.